<html>
<head><meta charset="utf-8"><title>Guarantee references from indexing arrays and slices? · t-lang · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/index.html">t-lang</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html">Guarantee references from indexing arrays and slices?</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="211078640"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211078640" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> isHavvy <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211078640">(Sep 24 2020 at 00:43)</a>:</h4>
<p>From <a href="https://old.reddit.com/r/rust/comments/ixqzkf/are_there_any_gotchas_to_converting_t_into_t_1/g6ch6el/?context=10000">Reddit</a>:</p>
<blockquote>
<p>This isn't relevant. There isn't a stated guarantee on how [T;N] makes its &amp;Ts. It could allocate space for a T on the heap, shuffle the fields of the correct element into that space, and return a pointer -- leaking the memory. Absurd? Doesn't matter. Doesn't even matter that I could come up with this example. It only matters that it's not stated.</p>
</blockquote>
<p>Do we have any guarantees about indexing into arrays and slices like this? And if not, is there a reason we can't/shouldn't?</p>



<a name="211078850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211078850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211078850">(Sep 24 2020 at 00:46)</a>:</h4>
<p>We do, I think. I'm not sure <em>where</em> but I would expect that this is something you can definitely rely on.</p>



<a name="211085687"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211085687" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211085687">(Sep 24 2020 at 03:04)</a>:</h4>
<p>The primitive slice docs seem clear to me</p>



<a name="211085690"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211085690" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211085690">(Sep 24 2020 at 03:05)</a>:</h4>
<blockquote>
<p>A dynamically-sized view into a contiguous sequence, [T]. Contiguous here means that elements are laid out so that every element is the same distance from its neighbors.</p>
</blockquote>



<a name="211085875"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211085875" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211085875">(Sep 24 2020 at 03:08)</a>:</h4>
<p>Oh, is that specifically about arrays? And they suppose that forming a slice could be a leaked heap allocation? Sheesh...</p>



<a name="211085888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211085888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211085888">(Sep 24 2020 at 03:09)</a>:</h4>
<p>Well, they're not wrong though, that's just so wild no one bothers to say "we don't do that"</p>



<a name="211085981"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211085981" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211085981">(Sep 24 2020 at 03:11)</a>:</h4>
<p><a href="https://doc.rust-lang.org/reference/types/array.html">https://doc.rust-lang.org/reference/types/array.html</a></p>



<a name="211086219"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211086219" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211086219">(Sep 24 2020 at 03:16)</a>:</h4>
<p>Yeah, nothing there <em>says</em> that the layout of the T values within an array must match the layout of the T values outside of the array.</p>



<a name="211086407"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211086407" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211086407">(Sep 24 2020 at 03:21)</a>:</h4>
<p>It's just "obviously" harder to do anything else</p>



<a name="211086491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211086491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211086491">(Sep 24 2020 at 03:23)</a>:</h4>
<p>Given things like <code>Cell</code>, the leak idea wouldn't even work, because there's no opportunity to copy updates back to your funky array layout</p>



<a name="211086502"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211086502" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211086502">(Sep 24 2020 at 03:23)</a>:</h4>
<p>Same for just <code>&amp;mut T</code>, actually</p>



<a name="211086506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211086506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211086506">(Sep 24 2020 at 03:23)</a>:</h4>
<p>Meh</p>



<a name="211087906"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211087906" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scottmcm <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211087906">(Sep 24 2020 at 03:55)</a>:</h4>
<p>I mean, you can do it in no-std no-alloc, so it's not allocate-plus-leak.</p>



<a name="211088457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211088457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> cuviper <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211088457">(Sep 24 2020 at 04:07)</a>:</h4>
<p>This is reminiscent of the horror of C++ <code>vector&lt;bool&gt;</code></p>



<a name="211108819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211108819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Daniel Henry-Mantilla <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211108819">(Sep 24 2020 at 09:42)</a>:</h4>
<p>FWIW, I think this belongs to Unsafe Code Guidelines. Indeed, the only way the distinction really matters is with <code>unsafe</code> code. If we had to add specifications about layout, they could fit there: <a href="https://rust-lang.github.io/unsafe-code-guidelines/layout/arrays-and-slices.html">https://rust-lang.github.io/unsafe-code-guidelines/layout/arrays-and-slices.html</a></p>



<a name="211223091"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211223091" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> isHavvy <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211223091">(Sep 25 2020 at 06:38)</a>:</h4>
<p>cc <span class="user-mention" data-user-id="120791">@RalfJ</span></p>



<a name="211227948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211227948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211227948">(Sep 25 2020 at 07:49)</a>:</h4>
<p>Cc <span class="user-group-mention" data-user-group-id="810">@WG-unsafe-code-guidelines</span></p>



<a name="211228004"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211228004" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211228004">(Sep 25 2020 at 07:50)</a>:</h4>
<p>as far as I am concerned, <a href="https://rust-lang.github.io/unsafe-code-guidelines/layout/arrays-and-slices.html">https://rust-lang.github.io/unsafe-code-guidelines/layout/arrays-and-slices.html</a> already says that the elements of a <code>[T]</code> are laid out like <code>T</code></p>



<a name="211228012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211228012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211228012">(Sep 25 2020 at 07:50)</a>:</h4>
<blockquote>
<p>Array types, [T; N], store N values of type T with a constant stride. Here, stride is the distance between each pair of consecutive values within the array.</p>
</blockquote>



<a name="211228026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211228026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211228026">(Sep 25 2020 at 07:50)</a>:</h4>
<p>I guess it could be more explicit and use the term "layout" instead of "type T", is that the question?</p>



<a name="211233879"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211233879" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> isHavvy <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211233879">(Sep 25 2020 at 09:07)</a>:</h4>
<p>It's the location of the reference generated by indexing into the array. That e.g. <code>&amp;array[2]</code> actually gives you an element from inside the array and not e.g. leaking a new value into existence.</p>



<a name="211248395"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211248395" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211248395">(Sep 25 2020 at 12:00)</a>:</h4>
<p>would it work to standardize that if <code>array: [T; N]</code> then <code>&amp;array[2]</code> is identical to <code>unsafe { (&amp;array as *const [T; N] as *const T).offset(2) as &amp;T }</code>?</p>



<a name="211248534"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211248534" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211248534">(Sep 25 2020 at 12:02)</a>:</h4>
<p>it would be better to do that on a formal syntax but the idea here is to indicate that it is literally the same as a pointer offset operation</p>



<a name="211248890"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211248890" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211248890">(Sep 25 2020 at 12:05)</a>:</h4>
<p>The UCG reference doesn't seem to describe primitive operations at all, only data layout. That should be another chapter of the book at least</p>



<a name="211353405"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211353405" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211353405">(Sep 26 2020 at 10:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="296643">isHavvy</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211233879">said</a>:</p>
<blockquote>
<p>It's the location of the reference generated by indexing into the array. That e.g. <code>&amp;array[2]</code> actually gives you an element from inside the array and not e.g. leaking a new value into existence.</p>
</blockquote>
<p>I don't think there woukld be opposition to guarantee that <code>&amp;array[x]</code> results in the same pointer as <code>&amp;*array.as_ptr().add(x)</code>. I am not sure what would be a good place to document this though... probably the slice type docs?</p>



<a name="211353455"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211353455" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211353455">(Sep 26 2020 at 10:20)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211248890">said</a>:</p>
<blockquote>
<p>The UCG reference doesn't seem to describe primitive operations at all, only data layout. That should be another chapter of the book at least</p>
</blockquote>
<p>UCG is mostly concerned with language-level question. this here is really a libs question.</p>



<a name="211360330"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360330" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360330">(Sep 26 2020 at 13:34)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> The behavior of primitive operations on primitive types seems very much like a language question. It is possible that <code>&amp;array[2]</code> gets desugared into a library call like <code>array.index(2)</code> but I would assume that this bottoms out to an intrinsic pretty quickly, and the behavior of that intrinsic is what I'm talking about</p>



<a name="211360413"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360413" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360413">(Sep 26 2020 at 13:36)</a>:</h4>
<p>I come from the land where languages are defined by a syntax and semantics. On the semantics side, UCG covers the definition of the abstract machine configuration (aka data layout), but not the operational semantics (aka primops)</p>



<a name="211360524"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360524" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360524">(Sep 26 2020 at 13:39)</a>:</h4>
<p>I cannot even think of another way to implementing the primitive operation that even makes the slightest sense^^ but, fair</p>



<a name="211360589"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360589" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360589">(Sep 26 2020 at 13:40)</a>:</h4>
<p>defining MIR operational semantics is something UCG and/or me want to get to eventually. however, most questions are fairly obvious and the ones that are not usually have open questions^^</p>



<a name="211360616"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360616" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360616">(Sep 26 2020 at 13:41)</a>:</h4>
<p>I think a good near term goal is to formally state all the obvious and uncontroversial things</p>



<a name="211360617"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360617" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360617">(Sep 26 2020 at 13:41)</a>:</h4>
<p>(I see defining MIR or simplified "pseudo-MIR" semantics as the best avenue for defining Rust semantics; we then can separately define how surface Rust translates to pseudo-MIR. that makes the entire thing much more manageable. this is a common approach for langauges with a large syntactic surface.)</p>



<a name="211360631"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360631" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360631">(Sep 26 2020 at 13:41)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360616">said</a>:</p>
<blockquote>
<p>I think a good near term goal is to formally state all the obvious and uncontroversial things</p>
</blockquote>
<p>yeah, I have wanted to start doing that several times. and then each time something more pressing came up.^^</p>



<a name="211360642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360642">(Sep 26 2020 at 13:41)</a>:</h4>
<p>I have some ideas for how I want things to be structured and phrased, but so far they are just rough ideas in my head</p>



<a name="211360679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360679">(Sep 26 2020 at 13:42)</a>:</h4>
<p>The post that started this thread seems to be exactly because we didn't state something that was obvious</p>



<a name="211360689"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360689" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360689">(Sep 26 2020 at 13:42)</a>:</h4>
<p>in particular, different people disagree on what "formally" means.^^ for me, it means "mechanized in Coq". ;)</p>



<a name="211360708"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360708" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360708">(Sep 26 2020 at 13:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360679">said</a>:</p>
<blockquote>
<p>The post that started this thread seems to be exactly because we didn't state something that was obvious</p>
</blockquote>
<p>yes. this is the first time such a question came up, compared to many many questions about data layout and validity (the two topics UCG discussed so far, before things basically stalled mid-way through the validity discussions)</p>



<a name="211360719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360719">(Sep 26 2020 at 13:43)</a>:</h4>
<p>I am on board with that, but actually I think it's not a replacement for the prose spec</p>



<a name="211360725"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360725" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360725">(Sep 26 2020 at 13:43)</a>:</h4>
<p>These are absolutely relevant questions, it's just a matter of priorization that their answers have not been written down yet</p>



<a name="211360790"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360790" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360790">(Sep 26 2020 at 13:44)</a>:</h4>
<p>I'm hoping that the UCG document eventually evolves to that prose spec</p>



<a name="211360801"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360801" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360801">(Sep 26 2020 at 13:44)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360719">said</a>:</p>
<blockquote>
<p>I am on board with that, but actually I think it's not a replacement for the prose spec</p>
</blockquote>
<p>agreed. though I am thinking of writing a spec in rust instead of prose, as prose tends to be wordy and imprecise.</p>



<a name="211360805"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360805" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360805">(Sep 26 2020 at 13:44)</a>:</h4>
<p>ideally with a coq formalization in the back <span aria-label="grinning face with smiling eyes" class="emoji emoji-1f601" role="img" title="grinning face with smiling eyes">:grinning_face_with_smiling_eyes:</span></p>



<a name="211360818"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360818" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360818">(Sep 26 2020 at 13:44)</a>:</h4>
<p>you can see a taste of that in <a href="https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/value-domain.md">https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/value-domain.md</a></p>



<a name="211360835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360835">(Sep 26 2020 at 13:45)</a>:</h4>
<p>(that still has more prose than I'd like, but you can see how I'd like to use Rust code to make things more precise but still readable without mathematical background)</p>



<a name="211360882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360882">(Sep 26 2020 at 13:46)</a>:</h4>
<p>yeah that looks nice</p>



<a name="211360896"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360896" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360896">(Sep 26 2020 at 13:46)</a>:</h4>
<p>What is your view on specs a la the C/C++ spec?</p>



<a name="211360898"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211360898" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211360898">(Sep 26 2020 at 13:47)</a>:</h4>
<p>i.e. language lawyer style</p>



<a name="211361107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211361107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> HeroicKatora <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211361107">(Sep 26 2020 at 13:51)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360801">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360719">said</a>:</p>
<blockquote>
<p>I am on board with that, but actually I think it's not a replacement for the prose spec</p>
</blockquote>
<p>agreed. though I am thinking of writing a spec in rust instead of prose, as prose tends to be wordy and imprecise.</p>
</blockquote>
<p>If that implies having the necessary means of writing self-tests in Rust that can be used to test alternative implementations then that would be very beneficial. I consider C++ spec particularly bad in this regard. While, yes, there is a sort of logic that you language lawyer, a very large amount of constraints are simply untestable—not necessarily undecidable but often requiring whole program analysis.</p>



<a name="211361226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211361226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211361226">(Sep 26 2020 at 13:54)</a>:</h4>
<p>I don't think the rust code snippets in Ralf's example are meant to compile</p>



<a name="211361307"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211361307" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211361307">(Sep 26 2020 at 13:56)</a>:</h4>
<p>Isn't unit testing the spec one of the possible uses of Miri?</p>



<a name="211364122"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211364122" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211364122">(Sep 26 2020 at 15:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211360896">said</a>:</p>
<blockquote>
<p>What is your view on specs a la the C/C++ spec?</p>
</blockquote>
<p>I am not a big fan. (a) I find it very hard to find anything, and (b) they leave many of the interesting questions open. the latter is mostly because these specs are <em>axiomatic</em>, not operational.</p>



<a name="211364154"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211364154" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211364154">(Sep 26 2020 at 15:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211361307">said</a>:</p>
<blockquote>
<p>Isn't unit testing the spec one of the possible uses of Miri?</p>
</blockquote>
<p>Miri is meant to basically be a compiling and running implementation of the spec -- with some concessions to performance</p>



<a name="211364416"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211364416" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211364416">(Sep 26 2020 at 15:08)</a>:</h4>
<p>however, that seems only loosely related to how testable the spec is? any spec with UB is hard to properly test for in a UB-exploiting compiler.</p>



<a name="211364791"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211364791" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211364791">(Sep 26 2020 at 15:17)</a>:</h4>
<p>for unit testing the spec though, you don't need a really good compiler, just one that detects UB in small examples</p>



<a name="211364800"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211364800" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211364800">(Sep 26 2020 at 15:17)</a>:</h4>
<p>so miri would work fine for that</p>



<a name="211367715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211367715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211367715">(Sep 26 2020 at 16:20)</a>:</h4>
<p>you mean detecting spec bugs? sure -- but that requires the spec to be in sync with miri, which is a strong assumption</p>



<a name="211367718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211367718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211367718">(Sep 26 2020 at 16:20)</a>:</h4>
<p>miri is still pretty hard to read I think, otehrwise I'd just propose it as the spec ;)</p>



<a name="211367958"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211367958" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211367958">(Sep 26 2020 at 16:27)</a>:</h4>
<blockquote>
<p>but that requires the spec to be in sync with miri, which is a strong assumption</p>
</blockquote>
<p>Is it? Right now I think miri is the closest thing we have to an actual spec</p>



<a name="211370587"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211370587" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211370587">(Sep 26 2020 at 17:29)</a>:</h4>
<p>sure, but once we have "two specs" (the markdown file with idealized rust and the actual thing in miri), they will inadvertantly diverge</p>



<a name="211370590"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211370590" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211370590">(Sep 26 2020 at 17:29)</a>:</h4>
<p>also miri does a few things different than the spec for perf reasons</p>



<a name="211372815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211372815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211372815">(Sep 26 2020 at 18:25)</a>:</h4>
<p>How essential are those compromises? Is it possible to have a "reference implementation" that is like miri but without the perf compromises, or are we talking impossibly slow? I think there is some value in using executable unit tests as a more programmer friendly way of explaining the technical details of a spec without the scary math or legalese</p>



<a name="211373020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211373020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211373020">(Sep 26 2020 at 18:30)</a>:</h4>
<p>cg_clif aborts on a few cases of UB instead of exploiting the UB. It by far doesn't check the majority of the UB things.</p>



<a name="211406559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406559">(Sep 27 2020 at 09:05)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211372815">said</a>:</p>
<blockquote>
<p>How essential are those compromises? Is it possible to have a "reference implementation" that is like miri but without the perf compromises, or are we talking impossibly slow? I think there is some value in using executable unit tests as a more programmer friendly way of explaining the technical details of a spec without the scary math or legalese</p>
</blockquote>
<p>I think it would probably still fast enough for tiny examples to run in &lt;1min</p>



<a name="211406570"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406570" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406570">(Sep 27 2020 at 09:05)</a>:</h4>
<p>but the problem is, to make Rust code actually run reduces readability a bit -- Rust's insistence on making the programmer care about pointer indirections and clones gets in the way here</p>



<a name="211406611"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406611" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406611">(Sep 27 2020 at 09:06)</a>:</h4>
<p>so I was aiming for a kind of pseudo-Rust -- some kind of ML with a Rusty syntax -- instead of something that can actually run</p>



<a name="211406619"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406619" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406619">(Sep 27 2020 at 09:06)</a>:</h4>
<p>oh and of course there's the question of how to handle non-determinism</p>



<a name="211406635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406635">(Sep 27 2020 at 09:07)</a>:</h4>
<p>even the document I linked above already has that, saying something like "pick a representation for the given abstract value"</p>



<a name="211406718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406718">(Sep 27 2020 at 09:09)</a>:</h4>
<p>I deliberately wrote the value relation as a <em>relation</em>, not a function, as I felt that makes it easier to understand... but this means it is not fully operational any more</p>



<a name="211406789"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406789" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406789">(Sep 27 2020 at 09:11)</a>:</h4>
<p>operationally however you need two functions, one that converts a byte string to an <code>Option&lt;Value&gt;</code> (computing the abstract value represented by this byte string, if any) and one that converts a value to a <code>impl Iterator&lt;Item=Bytes&gt;</code> (computing the possible ways this could be represented) and they need to be consistent with each other. such redundancy is necessary for a proper interpreter but IMO should be avoided in the spec.</p>



<a name="211406798"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211406798" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211406798">(Sep 27 2020 at 09:11)</a>:</h4>
<p>we should of course take care to define the relation in a way that these two functions are both computable</p>



<a name="211416766"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211416766" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211416766">(Sep 27 2020 at 13:31)</a>:</h4>
<p>Wouldn't a more natural way to represent nondeterminism be a call to a pseudorandom number generator?</p>



<a name="211416770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211416770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211416770">(Sep 27 2020 at 13:31)</a>:</h4>
<p>And for representing relations you can use a bool returning function</p>



<a name="211416942"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211416942" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211416942">(Sep 27 2020 at 13:36)</a>:</h4>
<p>Granted, these representations will not help very much for defining a miri-like exhaustive state enumeration without having exponential time complexity, but as long as the value of the code is only to be read and not executed (even if it is nominally executable) this would do the job pretty well, I think</p>



<a name="211417397"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417397" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417397">(Sep 27 2020 at 13:46)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211416766">said</a>:</p>
<blockquote>
<p>Wouldn't a more natural way to represent nondeterminism be a call to a pseudorandom number generator?</p>
</blockquote>
<p>that does not seem natural at all to me</p>



<a name="211417410"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417410" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417410">(Sep 27 2020 at 13:47)</a>:</h4>
<p>in formal methods, <code>X -&gt; list T</code>  is the canonical way to represent a computation with input <code>X</code> that non-deterministically produces one of the values of type <code>T</code> as a result. <code>list T</code> satisfies all the required monadic laws to make this a proper model of computation. Rust just doesn't have good support for this monad.^^</p>
<p>Also, non-determinism is something very different from randomness, so I am somewhat opposed to try and use one to model the other. these two concepts are already confused by too many people, which constantly annoys me.^^</p>



<a name="211417416"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417416" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417416">(Sep 27 2020 at 13:47)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211416770">said</a>:</p>
<blockquote>
<p>And for representing relations you can use a bool returning function</p>
</blockquote>
<p>yes but that doesnt make them computable. to write an interpreter we need to compute, given a value, some bytestring that relates to the value, and vice versa.</p>



<a name="211417720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417720">(Sep 27 2020 at 13:55)</a>:</h4>
<p>I am quite aware that nondeterminism is not randomness, but like it or not this is how most programmers conceptualize it. If you use a sufficiently good random number generator you can even get a completeness result if you run the program long enough</p>



<a name="211417777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417777">(Sep 27 2020 at 13:56)</a>:</h4>
<p>Perhaps rather than saying it is a random number generator, just use an opaque function called <code>nondeterministic()</code> and gloss it as "this is a nondeterministic value of the type"</p>



<a name="211417791"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417791" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417791">(Sep 27 2020 at 13:56)</a>:</h4>
<p>and you can implement that function for execution purposes as a random number generator, with comments explaining the limitations of this representation</p>



<a name="211417877"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417877" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417877">(Sep 27 2020 at 13:58)</a>:</h4>
<p>I would argue that X -&gt; list T is also not correct for nondeterminism because you could be selecting from an infinite advice string. X -&gt; 2^T is more correct</p>



<a name="211417960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211417960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211417960">(Sep 27 2020 at 14:00)</a>:</h4>
<p>X -&gt; list T is a good way to implement a program that enumerates all possible executions of a nondeterministic model, but the model itself is just a relation on states</p>



<a name="211418036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418036">(Sep 27 2020 at 14:02)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211417720">said</a>:</p>
<blockquote>
<p>I am quite aware that nondeterminism is not randomness, but like it or not this is how most programmers conceptualize it.</p>
</blockquote>
<p>I certainly dont like it and will push against anything that perpetuates this misunderstanding^^</p>



<a name="211418050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418050">(Sep 27 2020 at 14:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211417877">said</a>:</p>
<blockquote>
<p>I would argue that X -&gt; list T is also not correct for nondeterminism because you could be selecting from an infinite advice string. X -&gt; 2^T is more correct</p>
</blockquote>
<p>I guess I could weasle out of this by saying I meant haskell lists which can be infinite ;)</p>



<a name="211418055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418055">(Sep 27 2020 at 14:03)</a>:</h4>
<p>in Rust, <code>impl Iterator&lt;Item=T&gt;</code> is probably the closest approximation of that</p>



<a name="211418056"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418056" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418056">(Sep 27 2020 at 14:04)</a>:</h4>
<p>Even then, it's imposing an order of events that is not natural</p>



<a name="211418099"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418099" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418099">(Sep 27 2020 at 14:04)</a>:</h4>
<p>the order is not observable inside the monad though</p>



<a name="211418108"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418108" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418108">(Sep 27 2020 at 14:04)</a>:</h4>
<p>ah, well, if you've got a monad then that's fine, but you may as well use a monad for A -&gt; set T then</p>



<a name="211418118"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418118" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418118">(Sep 27 2020 at 14:05)</a>:</h4>
<p>but I think the important thing is that it looks like straight line code</p>



<a name="211418132"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418132" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418132">(Sep 27 2020 at 14:05)</a>:</h4>
<p>if you try to literally implement a A -&gt; list T function in rust it will have way too many unnecessary things for reading</p>



<a name="211418133"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418133" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418133">(Sep 27 2020 at 14:05)</a>:</h4>
<p>without support for general monads, Rust cannot make it look like straight-line code. well maybe with generators we can, but... uh</p>



<a name="211418136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418136">(Sep 27 2020 at 14:05)</a>:</h4>
<p>and anyway none of this matters because this is still a relation we cannot easily compute with</p>



<a name="211418174"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418174" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418174">(Sep 27 2020 at 14:06)</a>:</h4>
<p>Like I said, just have an opaque function</p>



<a name="211418177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418177">(Sep 27 2020 at 14:06)</a>:</h4>
<p>that works perfectly fine in rust</p>



<a name="211418186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418186">(Sep 27 2020 at 14:06)</a>:</h4>
<p>I mean besides being unimplementable, yeah</p>



<a name="211418192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418192">(Sep 27 2020 at 14:07)</a>:</h4>
<p>but also we have 3 or 4 levels down the rabbit hole at this point</p>



<a name="211418254"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418254" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418254">(Sep 27 2020 at 14:08)</a>:</h4>
<p>and you can even turn that into something executable with a whole lot of magic, where your calls to <code>nondeterministic()</code> build a graph behind the scenes and you traverse the graph</p>



<a name="211418260"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418260" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418260">(Sep 27 2020 at 14:08)</a>:</h4>
<p>(I think you are assuming that everything else is pure)</p>



<a name="211418263"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418263" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418263">(Sep 27 2020 at 14:08)</a>:</h4>
<p>specifically for the value relation, none of this is very useful as I think we should have a single relation and there's no computable way to get both forward and backward functions from that</p>



<a name="211418264"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418264" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418264">(Sep 27 2020 at 14:08)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418036">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211417720">said</a>:</p>
<blockquote>
<p>I am quite aware that nondeterminism is not randomness, but like it or not this is how most programmers conceptualize it.</p>
</blockquote>
<p>I certainly dont like it and will push against anything that perpetuates this misunderstanding^^</p>
</blockquote>
<p>what's the difference between the two?</p>



<a name="211418269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418269">(Sep 27 2020 at 14:09)</a>:</h4>
<p>(I'm one of those programmers :P)</p>



<a name="211418274"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418274" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418274">(Sep 27 2020 at 14:09)</a>:</h4>
<p>Nondeterminism is a set of options, randomness is a set of options with probabilities</p>



<a name="211418275"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418275" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418275">(Sep 27 2020 at 14:09)</a>:</h4>
<p>so in pseudo-code we can write</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="kd">let</span><span class="w"> </span><span class="n">rep</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">pick_value_such_that</span><span class="p">(</span><span class="o">|</span><span class="n">rep</span><span class="o">|</span><span class="w"> </span><span class="n">related</span><span class="p">(</span><span class="n">val</span><span class="p">,</span><span class="w"> </span><span class="n">rep</span><span class="p">))</span><span class="w"></span>
</code></pre></div>

<p>but we cannot actually implement this</p>



<a name="211418283"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418283" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418283">(Sep 27 2020 at 14:10)</a>:</h4>
<p>and pseudorandomness is a deterministic function that hits many of the options</p>



<a name="211418325"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418325" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418325">(Sep 27 2020 at 14:10)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418274">said</a>:</p>
<blockquote>
<p>Nondeterminism is a set of options, randomness is a set of options with probabilities</p>
</blockquote>
<p>I don't quite follow - is that different from having a set of options each with equal probability?</p>



<a name="211418327"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418327" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418327">(Sep 27 2020 at 14:10)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418274">said</a>:</p>
<blockquote>
<p>Nondeterminism is a set of options, randomness is a set of options with probabilities</p>
</blockquote>
<p>right -- randomness is basically a refinement of nondet. when a system is nondet you just say "a bunch of different things can happen", when you say a system is random you assume that there is a particular probabiltiy distribution that governs how often the various things happen. that is a strong assumption.</p>



<a name="211418332"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418332" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418332">(Sep 27 2020 at 14:11)</a>:</h4>
<p>randomness is <em>predictable</em></p>



<a name="211418345"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418345" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418345">(Sep 27 2020 at 14:11)</a>:</h4>
<p>I think we can comment our way around this issue though. Just put lots of warning signs saying "DON'T REASON ABOUT PROBABILITIES HERE"</p>



<a name="211418346"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418346" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418346">(Sep 27 2020 at 14:11)</a>:</h4>
<p>every random system can be turned into a nondet system by forgetting the probabilities; that loses a lot of information about the possible behaviors of the system. but nondet systems cannot always be described as random systems, because there's not always a probability distrubiton for their behavior.</p>



<a name="211418400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418400">(Sep 27 2020 at 14:12)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418345">said</a>:</p>
<blockquote>
<p>I think we can comment our way around this issue though. Just put lots of warning signs saying "DON'T REASON ABOUT PROBABILITIES HERE"</p>
</blockquote>
<p>sure we can but I'd rather not do that in a spec^^<br>
I am fine with just imagining that we are in the nondet monad though, and having a "pick a value from this set" or "pick a value satisfying this predicate" (predicate = Rust function returning <code>bool</code>)</p>



<a name="211418403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418403">(Sep 27 2020 at 14:12)</a>:</h4>
<p>At least for things a computer can do, it's always possible to give some probability distribution giving every possible option a nonzero probability</p>



<a name="211418419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418419">(Sep 27 2020 at 14:13)</a>:</h4>
<p><span class="user-mention silent" data-user-id="232545">Joshua Nelson</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418332">said</a>:</p>
<blockquote>
<p>randomness is <em>predictable</em></p>
</blockquote>
<p>yeah... that's a funny way to say it as people usually think of randomness as being about not having exact predictions, but you are right. you dont get exact predictions on individual outcomes but you do get increasingly exact predictions on increasingly large sets of outcomes.</p>



<a name="211418421"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418421" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418421">(Sep 27 2020 at 14:13)</a>:</h4>
<p>Yeah, from the spec point of view it's just an opaque function. The warning comments are for people who start poking into the framework code that makes the unit tests run and looks at the definition of <code>nondeterminism()</code> and sees something odd</p>



<a name="211418473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418473">(Sep 27 2020 at 14:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="232545">Joshua Nelson</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418325">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418274">said</a>:</p>
<blockquote>
<p>Nondeterminism is a set of options, randomness is a set of options with probabilities</p>
</blockquote>
<p>I don't quite follow - is that different from having a set of options each with equal probability?</p>
</blockquote>
<p>yes, very different. a system that whose spec is  "non-deterministically outputs 0 or 1" is correctly implemented by a program that does <code>print 0</code>. the same is obviously not true when the spec is "randomly output 0 or 1 with equal probability". the "equal probability" part puts a very strong constraint on what the system is allowed to do when you execute it many times.</p>



<a name="211418487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418487">(Sep 27 2020 at 14:15)</a>:</h4>
<p><a href="https://dilbert.com/strip/2001-10-25">https://dilbert.com/strip/2001-10-25</a></p>



<a name="211418489"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418489" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418489">(Sep 27 2020 at 14:15)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418421">said</a>:</p>
<blockquote>
<p>Yeah, from the spec point of view it's just an opaque function. The warning comments are for people who start poking into the framework code that makes the unit tests run and looks at the definition of <code>nondeterminism()</code> and sees something odd</p>
</blockquote>
<p>I honestly doubt we can have such framework code but this is an experiment worth doing^^</p>



<a name="211418540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418540">(Sep 27 2020 at 14:16)</a>:</h4>
<p>in particular in my pseudo-code I was going to just ignore the fact that Rust recursive types need to have pointer indirections. I dont want to write <code>Box</code> in our spec definitions ever.</p>



<a name="211418542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418542">(Sep 27 2020 at 14:16)</a>:</h4>
<p>but this means they cannot be legal Rust types</p>



<a name="211418608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418608">(Sep 27 2020 at 14:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418403">said</a>:</p>
<blockquote>
<p>At least for things a computer can do, it's always possible to give some probability distribution giving every possible option a nonzero probability</p>
</blockquote>
<p>we are talking about a spec (and its reference interpreter) though, and in a spec it makes a big difference whether we say "nondet" or "random". <br>
what you are saying is basically that true nondet does not exist in the real world, and I agree. the real world is a constant source of disappointment for only being able to approximate many of the beautiful things that exist in mathematics. ;)</p>



<a name="211418658"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418658" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418658">(Sep 27 2020 at 14:20)</a>:</h4>
<p>(lets skip the discussion whether true randomness exists ;)</p>



<a name="211418660"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418660" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418660">(Sep 27 2020 at 14:21)</a>:</h4>
<p>well, we're saying "nondet", it says it right there in the function name</p>



<a name="211418668"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418668" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418668">(Sep 27 2020 at 14:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418660">said</a>:</p>
<blockquote>
<p>well, we're saying "nondet", it says it right there in the function name</p>
</blockquote>
<p>yeah as I said, I am fine with using such an opaque function in the spec wording</p>



<a name="211418720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418720">(Sep 27 2020 at 14:22)</a>:</h4>
<p>the point about representability using randomness is only to point out that an implementation of nondet() using rand() is not wrong, in the sense that if the random number generator is perfect then if you run it long enough you will almost surely see all possible behaviors</p>



<a name="211418723"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418723" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418723">(Sep 27 2020 at 14:22)</a>:</h4>
<p>but the idealized Rust I have in my head as a spec language has other issues so actually running it will be hard for other reasons -- specifically, notice that in <a href="https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/value-domain.md">https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/value-domain.md</a> I define a recursive enum in a way that would not work in Rust</p>



<a name="211418734"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Guarantee%20references%20from%20indexing%20arrays%20and%20slices%3F/near/211418734" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F.html#211418734">(Sep 27 2020 at 14:23)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/213817-t-lang/topic/Guarantee.20references.20from.20indexing.20arrays.20and.20slices.3F/near/211418720">said</a>:</p>
<blockquote>
<p>the point about representability using randomness is only to point out that an implementation of nondet() using rand() is not wrong, in the sense that if the random number generator is perfect then if you run it long enough you will almost surely see all possible behaviors</p>
</blockquote>
<p>I agree that this is technically correct, and in fact Miri <a href="https://github.com/rust-lang/miri/blob/aa832c1133217a079ae5d9af65dd0b7ad96aca07/src/intptrcast.rs#L95">already does exactly that</a> (in a rather crude way even).<br>
So I think we mostly agree here except on details that are only worth discussing once there's actually something there. ;)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>